\begin{tabbing}
$\forall$$i$:Id, $T$:Type, $v$:$T$, $x$:Id.
\\[0ex]@$i$: $x$ : $T$ initially $x$ = $v$ $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: $x$ : $T$ initially $x$ = $v$ $\subseteq$ $D$ $\Rightarrow$ $D$ realizes ${\it es}$. vartype($i$;$x$) $\subseteq\rho$ $T$ \& $x$ initially@$i$  $=$ $v$)
\-
\end{tabbing}